\begin{tabbing}
$\forall$\=$D$:Dsys, ${\it sched}$:(Id$\rightarrow$($\mathbb{N}\rightarrow$(IdLnk+Id)+Unit)), $v$:($i$:Id$\rightarrow$M($i$).state),\+
\\[0ex]${\it dec}$:($i$,$a$:Id$\rightarrow$M($i$).state$\rightarrow$(M($i$).da(locl($a$))+Unit)).
\-\\[0ex]Feasible($D$)
\\[0ex]$\Rightarrow$ (\=$\forall$$i$:Id, $t$:$\mathbb{N}$.\+
\\[0ex]$\exists$$s$:M($i$).state.
\\[0ex]$s$ $=$ if $t$=$_{2}$0$\rightarrow$ $\lambda$$x$.M($i$).init($x$)?$v$($i$,$x$) else 1of(CV(d{-}comp($D$;$v$;${\it sched}$;${\it dec}$))($t$$-$1,$i$)) fi
\\[0ex]\& \=CV(d{-}comp($D$;$v$;${\it sched}$;${\it dec}$))($t$,$i$) $=$ stutter{-}state($s$) $\in$ d{-}world{-}state($D$;$i$)\+
\\[0ex]$\vee$ (\=$\exists$$k$:Knd, ${\it val}$:d{-}decl($D$;$i$)($k$).\+
\\[0ex]CV(d{-}comp($D$;$v$;${\it sched}$;${\it dec}$))($t$,$i$)
\\[0ex]$=$
\\[0ex]next{-}world{-}state($D$;$i$;$s$;$k$;${\it val}$)
\\[0ex]$\in$ d{-}world{-}state($D$;$i$)
\\[0ex]\& \=isrcv($k$)\+
\\[0ex]\& \=destination(lnk($k$)) $=$ $i$\+
\\[0ex]\& \=$\parallel$queue(lnk($k$);$t$)$\parallel\geq$1\+
\\[0ex]\& \=hd(queue(lnk($k$);$t$))\+
\\[0ex]$=$
\\[0ex]msg(lnk($k$);tag($k$);${\it val}$)
\\[0ex]$\in$ Msg($\lambda$$l$,${\it tg}$. M(source($l$)).dout($l$,${\it tg}$))
\-\-\-\\[0ex]$\vee$ islocal($k$)))
\-\-\-\-
\end{tabbing}